\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$L$:(event{-}info(${\it ds}$;${\it da}$) List). ecl{-}trans{-}state($v$; $L$) $\in$ ecl{-}trans{-}type($v$)
\-
\end{tabbing}